
#include "Node.h"

Node::Node(int a_n, int a_m): n(a_n), m(a_m), o(2*n*m), nbSelected(0), selectedVars(NULL)
{
	size_t memory_n = (n % 8 == 0 ? n / 8 : n / 8 + 1);
	size_t memory_m = (m % 8 == 0 ? m / 8 : m / 8 + 1);
	size_t memory_nm = (2*n*m % 8 == 0 ? 2*n*m / 8 : 2*n*m / 8 + 1);
	
	allocated_size = 1 + 2*memory_n + memory_m + memory_nm;
	bitmap = new char[allocated_size];
	memset(bitmap, 0, allocated_size);
	
	b1 = bitmap + 1;
	b2 = b1 + memory_n;
	b3 = b2 + memory_n;
	b4 = b3 + memory_m;
	
	set_solvable(true);
}

Node::Node(const Node &node): n(node.n), m(node.m), o(node.o), nbSelected(0), selectedVars(NULL)
{
	size_t memory_n = (n % 8 == 0 ? n / 8 : n / 8 + 1);
	size_t memory_m = (m % 8 == 0 ? m / 8 : m / 8 + 1);
	size_t memory_nm = (2*n*m % 8 == 0 ? 2*n*m / 8 : 2*n*m / 8 + 1);
	
	allocated_size = 1 + 2*memory_n + memory_m + memory_nm;
	bitmap = new char[allocated_size];
	memcpy(bitmap, node.bitmap, allocated_size);
	
	b1 = bitmap + 1;
	b2 = b1 + memory_n;
	b3 = b2 + memory_n;
	b4 = b3 + memory_m;
}

Node::Node(char *b, int a_n, int a_m): n(a_n), m(a_m), o(2*n*m), nbSelected(0), selectedVars(NULL)
{
	size_t memory_n = (n % 8 == 0 ? n / 8 : n / 8 + 1);
	size_t memory_m = (m % 8 == 0 ? m / 8 : m / 8 + 1);
	size_t memory_nm = (2*n*m % 8 == 0 ? 2*n*m / 8 : 2*n*m / 8 + 1);
	
	allocated_size = 1 + 2*memory_n + memory_m + memory_nm;
	bitmap = new char[allocated_size];
	
	b1 = bitmap + 1;
	b2 = b1 + memory_n;
	b3 = b2 + memory_n;
	b4 = b3 + memory_m;
	
	memcpy(bitmap, b, 1);
	memcpy(b1, b + 1, memory_n);
	memcpy(b2, b + memory_n + 1, memory_n);
	memcpy(b3, b + 2*memory_n + 1, memory_m);
	memcpy(b4, b +2*memory_n + memory_m + 1, memory_nm);
}

Node::~Node()
{
	delete[] bitmap;
	delete[] selectedVars;
}

void Node::printSolution()
{
	for(int i=0; i<n; i++)
	{
		cout<<varValues(i);
	}
	cout<<endl;
}

void Node::writeSolution(string file_name)
{
	ofstream file(file_name.c_str());

	if (file.fail())
	{
		cerr << "Error opening " << file_name << "." << endl;
		exit(EXIT_FAILURE);
	}

	if (isSolved())
	{
		file << "SAT" << endl;

		for (int v = 1; v <= n; v++)
		{
			if (varValues(v - 1))
			{
				file << v << " ";
			}
			else
			{
				file << -v << " ";
			}
		}

		file << 0 << endl;
	}
	else
	{
		file << "UNSAT" << endl;
	}

	file.close();
	if (file.fail())
	{
		cerr << "Error closing " << file_name << "." << endl;
		exit(EXIT_FAILURE);
	}
}

int Node::init_tautologies_elimination (ProblemData & data)
{
	int counter = 0;

	for (int c = 0; c < m; c++)
	{
		const set<int> & clause_literals = data.clauses[c];
		bool is_tautology = false;
		for (int v = 0; !is_tautology && v < n; v++)
		{
			if (clause_literals.find(v) != clause_literals.end() &&
				clause_literals.find(negation(v)) != clause_literals.end())
			{
				is_tautology = true;
			}
		}

		if (is_tautology)
		{
			data.eraseClause(c);
			set_solvedClauses(c, true);
			counter++;
		}
	}

	return counter;
}

int Node::init_unit_propagation (ProblemData & data)
{
	int counter = 0;

	for (map<int, set<int> >::const_iterator c_it = data.clauses.begin(),
		 c_it_end = data.clauses.end(); isSolvable() && c_it != c_it_end; )
	{
		/* If the current clause is empty, then the formula isn't satisfiable.
		 */
		if (c_it->second.size() == 0)
		{
			set_solvable(false);
		}

		/* Else, if the current clause has one unique literal */
		else if (c_it->second.size() == 1)
		{
			int id = *c_it->second.begin();

			/* Remove all the satisfied clauses. */
			for (set<int>::const_iterator l_it = data.literals[id].begin(),
				 l_it_end = data.literals[id].end(); l_it != l_it_end; )
			{
				set_solvedClauses(*l_it, true);
				data.eraseClause(*l_it++);
			}

			/* Remove the unique literal's negation from all the clauses
			   containing it, and clear its clauses list.
			 */
			int not_id = negation(id);
			for (set<int>::const_iterator l_it = data.literals[not_id].begin(),
				 l_it_end = data.literals[not_id].end(); l_it != l_it_end;
				 ++l_it)
			{
				data.clauses[*l_it].erase(not_id);
			}
			data.literals[not_id].clear();

			/* Affect the variable to the right value. */
			if (id < n)
			{
				if(!varAffected(id))
				{
					set_varAffected(id, true);
					set_varValues(id, true);
				}
				else if(!varValues(id))
				{
					set_solvable(false);
				}
			}
			else
			{
				id = negation(id);
				if(!varAffected(id))
				{
					set_varAffected(id, true);
					set_varValues(id, false);
				}
				else if(varValues(id))
				{
					set_solvable(false);
				}
			}

			/* Force the loop to restart from the beginning. */
			c_it = data.clauses.begin();
			counter++;
		}

		/* Else, the clause contains more than one literal, continue iterating
		   over the remaining clauses.
		 */
		else
		{
			++c_it;
		}
	}

	return counter;
}

int Node::init_pure_literals_elimination (ProblemData & data)
{
	int counter = 0;

	/* For each unaffected variable */
	for (int v = 0; isSolvable() && v < n; v++)
	{
		if (!varAffected(v))
		{
			/* If the variable doesn't appear anywhere anymore, affect it to
			   false.
			 */
			if ((data.literals[v].size() == 0) &&
				(data.literals[negation(v)].size() == 0))
			{
				set_varAffected(v, true);
				set_varValues(v, false);
			}

			/* Else, if the positive form of the variable is a pure literal (the
			   negative form does not appear), affect the variable to true and
			   remove all the newly satisfied clauses. Restart the loop from the
			   beginning.
			 */
			else if (data.literals[negation(v)].size() == 0)
			{
				set_varAffected(v, true);
				set_varValues(v, true);

				for (set<int>::const_iterator it = data.literals[v].begin(),
					 it_end = data.literals[v].end(); it != it_end; )
				{
					set_solvedClauses(*it, true);
					data.eraseClause(*it++);
				}
				v = -1;

				counter++;
			}

			/* Else, if the negative form of the variable is a pure literal (the
			   positive form does not appear), affect the variable to false and
			   remove all the newly satisfied clauses. Restart the loop from the
			   beginning.
			 */
			else if (data.literals[v].size() == 0)
			{
				set_varAffected(v, true);
				set_varValues(v, false);

				int not_v = negation(v);
				for (set<int>::const_iterator it = data.literals[not_v].begin(),
					 it_end = data.literals[not_v].end(); it != it_end; )
				{
					set_solvedClauses(*it, true);
					data.eraseClause(*it++);
				}
				v = -1;

				counter++;
			}
		}
	}

	return counter;
}

Node Node::getFirstNode(ProblemData data)
{
	bool solvable = true;
	Node node(data.nLiterals/2, data.nClauses);

	/* Perform the initial simplifications. */
	cout << endl << "Performing initial simplifications..." << endl;
	cout << "Removed " << node.init_tautologies_elimination(data)
		 << " tautologies." << endl;
	
	int c_unit, c_pure, temp;
	c_unit = node.init_unit_propagation(data);
	temp = c_pure = node.init_pure_literals_elimination(data);
	
	while(temp != 0)
	{
		temp = node.init_unit_propagation(data);
		c_unit += temp;
		
		if(temp != 0)
		{
			temp = node.init_pure_literals_elimination(data);
			c_pure += temp;
		}
	}
	
	cout << "Performed " << c_unit << " unit propagations." << endl;
	cout << "Performed " << c_pure << " pure literals eliminations." << endl;

	/* Check if the formula is now satisfied. */
	bool solved = true;
	for (int c = 0; solved && c < node.m; c++)
	{
		if (!node.solvedClauses(c))
		{
			solved = false;
		}
	}
	
	/* If the formula is now satisfied, just indicate that it is. */
	if (solved)
	{
		node.set_solved(true);
	}
	/* Else, initialize the bitmap indicating the literals that are in each
	   clause.
	 */
	else
	{
		for (map<int, set<int> >::const_iterator c_it = data.clauses.begin(),
			 c_it_end = data.clauses.end(); solvable && c_it != c_it_end; ++c_it)
		{
			for(set<int>::const_iterator l_it = c_it->second.begin(),
				l_it_end = c_it->second.end(); l_it != l_it_end; ++l_it)
			{
				node.set_clauseLiterals(c_it->first, *l_it, true);
			}
		}
	}
	
	return(node);
}

Node Node::exploreOne(char* b, int *vars, int n, int m, int N, int i)
{
	Node result(b,n,m);
	
	//First, we build a list of variables to affect
	list<int> toAffect;
	for(int j = 0; j<N; j++)
	{
		toAffect.push_back(vars[j]);
	}
	
	//Then, we use index of the new node to determine which variables will be set to true or false
	list<bool> temp;
	
	for(int j=0; j < N; j++)
	{
		if((i & (1<<j)) != 0)
		{
			temp.push_back(true);
		}
		else
		{
			temp.push_back(false);
		}
	}
	
	//This variable will let us know when a clause
	//will have been statisfied, so that we can check
	//if the problem is solved
	bool solvedOneClause = false;
	
	//List of conditions that may help propagate the affectation
	list<int> toPropagate;
	//List of clauses that were just solved
	list<int> recentlySolved;

	
	int currentVar;
	bool currentValue;
	
	while(!toAffect.empty())
	{
		currentVar = toAffect.front();
		currentValue = temp.front();
		toAffect.pop_front();
		temp.pop_front();
		
		//We check that there is no conflict in affectations
		if(result.varAffected(currentVar))
		{
			if(result.varValues(currentVar) != currentValue)
			{
				result.set_solvable(false);
				return(result);
			}
			else
			{
				continue;
			}
		}
		
		//If not, we can affect it
		result.set_varAffected(currentVar,true);
		result.set_varValues(currentVar, currentValue);
		
		//Each time we affect a variable, we check the unsatisfied clauses containing it
		for(int k=0; k < m; k++)
		{
			if(!result.solvedClauses(k))
			{
				//If the affectation did not satisfy the clause, we remove the variable
				//from the remaining literals of the clause. If it did, we mark the clause
				//as satisfied
				if(result.clauseLiterals(k, currentVar))
				{
					if(currentValue)
					{
						result.set_solvedClauses(k, true);
						solvedOneClause = true;
						recentlySolved.push_back(k);
					}
					else
					{
						toPropagate.push_back(k);
						result.set_clauseLiterals(k, currentVar, false);
					}
				}
				else if(result.clauseLiterals(k, result.negation(currentVar)))
				{
					if(!currentValue)
					{
						result.set_solvedClauses(k, true);
						solvedOneClause = true;
						recentlySolved.push_back(k);
					}
					else
					{
						toPropagate.push_back(k);
						result.set_clauseLiterals(k, result.negation(currentVar), false);
					}
				}
			}
		}
		
		//Now for the propagation
		int k, remainingLiterals, variable;
		bool valVariable;
		
		while(!toPropagate.empty())
		{
			k = toPropagate.front();
			toPropagate.pop_front();
			
			//We count the number of remaining literals in the modified clauses
			remainingLiterals = 0;
			
			for(int l=0; l<2*n; l++)
			{
				if(result.clauseLiterals(k, l))
				{
					remainingLiterals++;
					if(remainingLiterals > 1)
					{
						break;
					}
					
					if(l<result.n)
					{
						variable = l;
						valVariable = true;
					}
					else
					{
						variable = result.negation(l);
						valVariable = false;
					}
				}
			}
			
			//If there are no literals left, the node is not solvable
			//If there is only one left, we can affect it
			if(remainingLiterals == 0)
			{
				result.set_solvable(false);
				return(result);
			}
			else if (remainingLiterals == 1)
			{
				toAffect.push_back(variable);
				temp.push_back(valVariable);
			}
		}
		
		//Now we will affect literals which don't have their negations in the formula anymore
		vector<bool> possiblyDisappeared(2*n, false);
		int possiblyDisappearedNumber = 0;
		
		// Get the literals that have possibly disappeared from the clauses that
		// were solved during that iteration of the loop
		while(toAffect.empty() && !recentlySolved.empty())
		{
			k = recentlySolved.front();
			recentlySolved.pop_front();
			
			for(int l=0; l<2*n; l++)
			{
				if (l < n && !result.varAffected(l) ||
					l >= n && !result.varAffected(result.negation(l)))
				{
					if(result.clauseLiterals(k, l))
					{
						if(!possiblyDisappeared[l])
						{
							possiblyDisappeared[l] = true;
							possiblyDisappearedNumber++;
						}
					}
				}
			}
		}
		
		// Now get the literals that have really disappeared from those that
		// have possibly disappeared
		if(possiblyDisappearedNumber > 0)
		{
			for(k=0; k < m; k++)
			{
				if(!result.solvedClauses(k))
				{
					for(int l=0; l<2*n; l++)
					{
						if(result.clauseLiterals(k, l))
						{
							if(possiblyDisappeared[l])
							{
								possiblyDisappeared[l] = false;
								possiblyDisappearedNumber--;
								if(possiblyDisappearedNumber == 0)
								{
									break;
								}
							}
						}
					}
				}
			}
		}
		
		// For all literals that have disappeared, affect its negation
		// (therefore a pure literal) to true
		if(possiblyDisappearedNumber > 0)
		{
			for(k=0; k<2*n; k++)
			{
				if(possiblyDisappeared[k])
				{
					if(k<n)
					{
						toAffect.push_back(k);
						temp.push_back(false);
					}
					else
					{
						toAffect.push_back(result.negation(k));
						temp.push_back(true);
					}
				}
			}
		}
		
	}
	
	//If we have satisfied a new clause, we check if the problem is solved
	if(result.isSolvable() && solvedOneClause)
	{
		result.set_solved(true);
		for(int j=0; j < m; j++)
		{
			if(!result.solvedClauses(j))
			{
				result.set_solved(false);
				break;
			}
		}
	}
	
	return(result);
}

vector<Node> Node::explore(unsigned int N)
{
	vector<Node> result;
	
	/* First simplify the current node, if the formula has been satisfied by
	 simplification, just return the current node.
	 */
	if (isSolved())
	{
		result.push_back(*this);
	}
	
	/* Else, branch on the given number of next unaffected variables. */
	else
	{
		unaffected(N);
		
		if(isSolvable())    //If the problem is not solvable, we don't create new nodes
		{
			//We branch on vars.size() binary variables
			int nbNewNodes = pow(2,nbSelected);
			
			for (int i=0; i < nbNewNodes; i++)
			{
				Node node = exploreOne(bitmap, selectedVars, n, m, nbSelected, i);
				if(node.isSolvable())
				{
					result.push_back(node);
				}
			}
		}
	}
	
	return(result);
}
